The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

g(x, x, x) → g(c, d, e)
g(x, y, x) → g(c, d, e)
s(f(x, y)) → f(y, f(s(s(x)), a))
h(h(x, a), y) → h(h(a, y), h(a, x))
f(x, f(y, f(x, y))) → f(a, f(x, f(y, b)))
f(h(a, y), g(x, b, a)) → h(f(x, s(y)), s(b))
h(f(x, s(y)), b) → f(a, g(y, a, f(s(x), a)))
f(x, g(x, a, f(s(x), y))) → f(h(x, b), g(a, b, y))
s(y) → b

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

G(z0, z0, z0) → c1(G(c, d, e))
G(z0, z1, z0) → c2(G(c, d, e))
S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
H(f(z0, s(z1)), b) → c6(F(a, g(z1, a, f(s(z0), a))), G(z1, a, f(s(z0), a)), F(s(z0), a), S(z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))
F(z0, g(z0, a, f(s(z0), z1))) → c9(F(h(z0, b), g(a, b, z1)), H(z0, b), G(a, b, z1))

S tuples:

G(z0, z0, z0) → c1(G(c, d, e))
G(z0, z1, z0) → c2(G(c, d, e))
S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
H(f(z0, s(z1)), b) → c6(F(a, g(z1, a, f(s(z0), a))), G(z1, a, f(s(z0), a)), F(s(z0), a), S(z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))
F(z0, g(z0, a, f(s(z0), z1))) → c9(F(h(z0, b), g(a, b, z1)), H(z0, b), G(a, b, z1))

K tuples:none
Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

G, S, H, F

Compound Symbols:

c1, c2, c3, c5, c6, c7, c8, c9

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

F(z0, g(z0, a, f(s(z0), z1))) → c9(F(h(z0, b), g(a, b, z1)), H(z0, b), G(a, b, z1))
H(f(z0, s(z1)), b) → c6(F(a, g(z1, a, f(s(z0), a))), G(z1, a, f(s(z0), a)), F(s(z0), a), S(z0))

Removed 2 trailing nodes:

G(z0, z1, z0) → c2(G(c, d, e))
G(z0, z0, z0) → c1(G(c, d, e))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

S tuples:

S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

K tuples:none
Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

S, H, F

Compound Symbols:

c3, c5, c7, c8

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

We considered the (Usable) Rules:

s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))

And the Tuples:

S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x₁, x₂)) = [2]x₂   
POL(H(x₁, x₂)) = 0   
POL(S(x₁)) = 0   
POL(a) = 0   
POL(b) = 0   
POL(c3(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄   
POL(c5(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c8(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄   
POL(f(x₁, x₂)) = 0   
POL(g(x₁, x₂, x₃)) = [3] + [5]x₁   
POL(h(x₁, x₂)) = [3]   
POL(s(x₁)) = 0   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

S tuples:

S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))

K tuples:

F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

S, H, F

Compound Symbols:

c3, c5, c7, c8

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0)) by

S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
S(f(x0, x1)) → c3

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))
S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
S(f(x0, x1)) → c3

S tuples:

H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
S(f(x0, x1)) → c3

K tuples:

F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

H, F, S

Compound Symbols:

c5, c7, c8, c3, c3

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

S(f(x0, x1)) → c3

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))
S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))

S tuples:

H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))

K tuples:

F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

H, F, S

Compound Symbols:

c5, c7, c8, c3

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0)) by

H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))
S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))

S tuples:

F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))

K tuples:

F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

F, S, H

Compound Symbols:

c7, c8, c3, c5

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b)) by

F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))
S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))

S tuples:

S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))

K tuples:

F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

F, S, H

Compound Symbols:

c8, c3, c5, c7

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b)) by

F(h(a, x0), g(x1, b, a)) → c8(H(f(x1, s(x0)), b), F(x1, s(x0)), S(x0), S(b))
F(h(a, f(z0, z1)), g(x1, b, a)) → c8(H(f(x1, f(z1, f(s(s(z0)), a))), s(b)), F(x1, s(f(z0, z1))), S(f(z0, z1)), S(b))
F(h(a, z0), g(x1, b, a)) → c8(H(f(x1, b), s(b)), F(x1, s(z0)), S(z0), S(b))
F(h(a, x0), g(x1, b, a)) → c8

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))
F(h(a, x0), g(x1, b, a)) → c8(H(f(x1, s(x0)), b), F(x1, s(x0)), S(x0), S(b))
F(h(a, f(z0, z1)), g(x1, b, a)) → c8(H(f(x1, f(z1, f(s(s(z0)), a))), s(b)), F(x1, s(f(z0, z1))), S(f(z0, z1)), S(b))
F(h(a, z0), g(x1, b, a)) → c8(H(f(x1, b), s(b)), F(x1, s(z0)), S(z0), S(b))
F(h(a, x0), g(x1, b, a)) → c8

S tuples:

S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))

K tuples:

F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))

Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

S, H, F

Compound Symbols:

c3, c5, c7, c8, c8

(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(h(a, x0), g(x1, b, a)) → c8

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))
F(h(a, x0), g(x1, b, a)) → c8(H(f(x1, s(x0)), b), F(x1, s(x0)), S(x0), S(b))
F(h(a, f(z0, z1)), g(x1, b, a)) → c8(H(f(x1, f(z1, f(s(s(z0)), a))), s(b)), F(x1, s(f(z0, z1))), S(f(z0, z1)), S(b))
F(h(a, z0), g(x1, b, a)) → c8(H(f(x1, b), s(b)), F(x1, s(z0)), S(z0), S(b))

S tuples:

S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))

K tuples:none
Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

S, H, F

Compound Symbols:

c3, c5, c7, c8

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0)) by

S(f(x0, x1)) → c3(F(s(s(x0)), a), S(s(x0)), S(x0))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))
F(h(a, x0), g(x1, b, a)) → c8(H(f(x1, s(x0)), b), F(x1, s(x0)), S(x0), S(b))
F(h(a, f(z0, z1)), g(x1, b, a)) → c8(H(f(x1, f(z1, f(s(s(z0)), a))), s(b)), F(x1, s(f(z0, z1))), S(f(z0, z1)), S(b))
F(h(a, z0), g(x1, b, a)) → c8(H(f(x1, b), s(b)), F(x1, s(z0)), S(z0), S(b))
S(f(x0, x1)) → c3(F(s(s(x0)), a), S(s(x0)), S(x0))

S tuples:

S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1)))
S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))
S(f(x0, x1)) → c3(F(s(s(x0)), a), S(s(x0)), S(x0))

K tuples:none
Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

S, H, F

Compound Symbols:

c3, c5, c7, c8, c3

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace S(f(f(z0, z1), x1)) → c3(F(x1, f(s(f(z1, f(s(s(z0)), a))), a)), F(s(s(f(z0, z1))), a), S(s(f(z0, z1))), S(f(z0, z1))) by

S(f(f(x0, z0), x2)) → c3(F(x2, f(f(f(s(s(x0)), a), f(s(s(z0)), a)), a)), F(s(s(f(x0, z0))), a), S(s(f(x0, z0))), S(f(x0, z0)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(b, a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(s(f(x1, f(b, a))), a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(f(z0, z1), x1), x2)) → c3(F(x2, f(s(f(x1, f(s(f(z1, f(s(s(z0)), a))), a))), a)), F(s(s(f(f(z0, z1), x1))), a), S(s(f(f(z0, z1), x1))), S(f(f(z0, z1), x1)))
S(f(f(z0, x1), x2)) → c3(F(x2, f(s(f(x1, f(s(b), a))), a)), F(s(s(f(z0, x1))), a), S(s(f(z0, x1))), S(f(z0, x1)))
S(f(f(x0, x1), x2)) → c3(F(s(s(f(x0, x1))), a), S(s(f(x0, x1))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))
F(h(a, x0), g(x1, b, a)) → c8(H(f(x1, s(x0)), b), F(x1, s(x0)), S(x0), S(b))
F(h(a, f(z0, z1)), g(x1, b, a)) → c8(H(f(x1, f(z1, f(s(s(z0)), a))), s(b)), F(x1, s(f(z0, z1))), S(f(z0, z1)), S(b))
F(h(a, z0), g(x1, b, a)) → c8(H(f(x1, b), s(b)), F(x1, s(z0)), S(z0), S(b))
S(f(x0, x1)) → c3(F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(x0, z0), x2)) → c3(F(x2, f(f(f(s(s(x0)), a), f(s(s(z0)), a)), a)), F(s(s(f(x0, z0))), a), S(s(f(x0, z0))), S(f(x0, z0)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(b, a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(s(f(x1, f(b, a))), a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(f(z0, z1), x1), x2)) → c3(F(x2, f(s(f(x1, f(s(f(z1, f(s(s(z0)), a))), a))), a)), F(s(s(f(f(z0, z1), x1))), a), S(s(f(f(z0, z1), x1))), S(f(f(z0, z1), x1)))
S(f(f(z0, x1), x2)) → c3(F(x2, f(s(f(x1, f(s(b), a))), a)), F(s(s(f(z0, x1))), a), S(s(f(z0, x1))), S(f(z0, x1)))
S(f(f(x0, x1), x2)) → c3(F(s(s(f(x0, x1))), a), S(s(f(x0, x1))))

S tuples:

S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))
S(f(x0, x1)) → c3(F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(x0, z0), x2)) → c3(F(x2, f(f(f(s(s(x0)), a), f(s(s(z0)), a)), a)), F(s(s(f(x0, z0))), a), S(s(f(x0, z0))), S(f(x0, z0)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(b, a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(s(f(x1, f(b, a))), a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(f(z0, z1), x1), x2)) → c3(F(x2, f(s(f(x1, f(s(f(z1, f(s(s(z0)), a))), a))), a)), F(s(s(f(f(z0, z1), x1))), a), S(s(f(f(z0, z1), x1))), S(f(f(z0, z1), x1)))
S(f(f(z0, x1), x2)) → c3(F(x2, f(s(f(x1, f(s(b), a))), a)), F(s(s(f(z0, x1))), a), S(s(f(z0, x1))), S(f(z0, x1)))
S(f(f(x0, x1), x2)) → c3(F(s(s(f(x0, x1))), a), S(s(f(x0, x1))))

K tuples:none
Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

S, H, F

Compound Symbols:

c3, c5, c7, c8, c3, c3

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace S(f(z0, x1)) → c3(F(x1, f(s(b), a)), F(s(s(z0)), a), S(s(z0)), S(z0)) by

S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(x0, x1)) → c3(F(s(s(x0)), a), S(s(x0)), S(x0))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))

Tuples:

H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))
F(h(a, x0), g(x1, b, a)) → c8(H(f(x1, s(x0)), b), F(x1, s(x0)), S(x0), S(b))
F(h(a, f(z0, z1)), g(x1, b, a)) → c8(H(f(x1, f(z1, f(s(s(z0)), a))), s(b)), F(x1, s(f(z0, z1))), S(f(z0, z1)), S(b))
F(h(a, z0), g(x1, b, a)) → c8(H(f(x1, b), s(b)), F(x1, s(z0)), S(z0), S(b))
S(f(x0, x1)) → c3(F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(x0, z0), x2)) → c3(F(x2, f(f(f(s(s(x0)), a), f(s(s(z0)), a)), a)), F(s(s(f(x0, z0))), a), S(s(f(x0, z0))), S(f(x0, z0)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(b, a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(s(f(x1, f(b, a))), a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(f(z0, z1), x1), x2)) → c3(F(x2, f(s(f(x1, f(s(f(z1, f(s(s(z0)), a))), a))), a)), F(s(s(f(f(z0, z1), x1))), a), S(s(f(f(z0, z1), x1))), S(f(f(z0, z1), x1)))
S(f(f(z0, x1), x2)) → c3(F(x2, f(s(f(x1, f(s(b), a))), a)), F(s(s(f(z0, x1))), a), S(s(f(z0, x1))), S(f(z0, x1)))
S(f(f(x0, x1), x2)) → c3(F(s(s(f(x0, x1))), a), S(s(f(x0, x1))))
S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))

S tuples:

H(h(x0, a), x1) → c5(H(h(a, x1), h(a, x0)))
F(x0, f(x1, f(x0, x1))) → c7(F(a, f(x0, f(x1, b))))
S(f(x0, x1)) → c3(F(s(s(x0)), a), S(s(x0)), S(x0))
S(f(f(x0, z0), x2)) → c3(F(x2, f(f(f(s(s(x0)), a), f(s(s(z0)), a)), a)), F(s(s(f(x0, z0))), a), S(s(f(x0, z0))), S(f(x0, z0)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(b, a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(x0, x1), x2)) → c3(F(x2, f(s(f(x1, f(b, a))), a)), F(s(s(f(x0, x1))), a), S(s(f(x0, x1))), S(f(x0, x1)))
S(f(f(f(z0, z1), x1), x2)) → c3(F(x2, f(s(f(x1, f(s(f(z1, f(s(s(z0)), a))), a))), a)), F(s(s(f(f(z0, z1), x1))), a), S(s(f(f(z0, z1), x1))), S(f(f(z0, z1), x1)))
S(f(f(z0, x1), x2)) → c3(F(x2, f(s(f(x1, f(s(b), a))), a)), F(s(s(f(z0, x1))), a), S(s(f(z0, x1))), S(f(z0, x1)))
S(f(f(x0, x1), x2)) → c3(F(s(s(f(x0, x1))), a), S(s(f(x0, x1))))
S(f(x0, x1)) → c3(F(x1, f(b, a)), F(s(s(x0)), a), S(s(x0)), S(x0))

K tuples:none
Defined Rule Symbols:

g, s, h, f

Defined Pair Symbols:

H, F, S

Compound Symbols:

c5, c7, c8, c3, c3, c3

(25) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match(-raise)-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match(-raise)-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 11]
transitions:
a0() → 0
g0(0, 0, 0) → 1
s0(0) → 2
h0(0, 0) → 3
f0(0, 0) → 4
c1() → 5
d1() → 6
e1() → 7
g1(5, 6, 7) → 1
c1() → 0
d1() → 0
e1() → 0
b1() → 2
b1() → 0
c1() → 8
d1() → 9
e1() → 10
b1() → 11
g0(8, 0, 0) → 1
g0(0, 8, 0) → 1
g0(0, 0, 8) → 1
g0(9, 0, 0) → 1
g0(0, 9, 0) → 1
g0(0, 0, 9) → 1
g0(10, 0, 0) → 1
g0(0, 10, 0) → 1
g0(0, 0, 10) → 1
g0(11, 0, 0) → 1
g0(0, 11, 0) → 1
g0(0, 0, 11) → 1
g0(8, 8, 0) → 1
g0(8, 0, 8) → 1
g0(8, 9, 0) → 1
g0(8, 0, 9) → 1
g0(8, 10, 0) → 1
g0(8, 0, 10) → 1
g0(8, 11, 0) → 1
g0(8, 0, 11) → 1
g0(0, 8, 8) → 1
g0(9, 8, 0) → 1
g0(0, 8, 9) → 1
g0(10, 8, 0) → 1
g0(0, 8, 10) → 1
g0(11, 8, 0) → 1
g0(0, 8, 11) → 1
g0(9, 0, 8) → 1
g0(0, 9, 8) → 1
g0(10, 0, 8) → 1
g0(0, 10, 8) → 1
g0(11, 0, 8) → 1
g0(0, 11, 8) → 1
g0(9, 9, 0) → 1
g0(9, 0, 9) → 1
g0(9, 10, 0) → 1
g0(9, 0, 10) → 1
g0(9, 11, 0) → 1
g0(9, 0, 11) → 1
g0(0, 9, 9) → 1
g0(10, 9, 0) → 1
g0(0, 9, 10) → 1
g0(11, 9, 0) → 1
g0(0, 9, 11) → 1
g0(10, 0, 9) → 1
g0(0, 10, 9) → 1
g0(11, 0, 9) → 1
g0(0, 11, 9) → 1
g0(10, 10, 0) → 1
g0(10, 0, 10) → 1
g0(10, 11, 0) → 1
g0(10, 0, 11) → 1
g0(0, 10, 10) → 1
g0(11, 10, 0) → 1
g0(0, 10, 11) → 1
g0(11, 0, 10) → 1
g0(0, 11, 10) → 1
g0(11, 11, 0) → 1
g0(11, 0, 11) → 1
g0(0, 11, 11) → 1
g0(8, 8, 8) → 1
g0(8, 8, 9) → 1
g0(8, 8, 10) → 1
g0(8, 8, 11) → 1
g0(8, 9, 8) → 1
g0(8, 10, 8) → 1
g0(8, 11, 8) → 1
g0(8, 9, 9) → 1
g0(8, 9, 10) → 1
g0(8, 9, 11) → 1
g0(8, 10, 9) → 1
g0(8, 11, 9) → 1
g0(8, 10, 10) → 1
g0(8, 10, 11) → 1
g0(8, 11, 10) → 1
g0(8, 11, 11) → 1
g0(9, 8, 8) → 1
g0(10, 8, 8) → 1
g0(11, 8, 8) → 1
g0(9, 8, 9) → 1
g0(9, 8, 10) → 1
g0(9, 8, 11) → 1
g0(10, 8, 9) → 1
g0(11, 8, 9) → 1
g0(10, 8, 10) → 1
g0(10, 8, 11) → 1
g0(11, 8, 10) → 1
g0(11, 8, 11) → 1
g0(9, 9, 8) → 1
g0(9, 10, 8) → 1
g0(9, 11, 8) → 1
g0(10, 9, 8) → 1
g0(11, 9, 8) → 1
g0(10, 10, 8) → 1
g0(10, 11, 8) → 1
g0(11, 10, 8) → 1
g0(11, 11, 8) → 1
g0(9, 9, 9) → 1
g0(9, 9, 10) → 1
g0(9, 9, 11) → 1
g0(9, 10, 9) → 1
g0(9, 11, 9) → 1
g0(9, 10, 10) → 1
g0(9, 10, 11) → 1
g0(9, 11, 10) → 1
g0(9, 11, 11) → 1
g0(10, 9, 9) → 1
g0(11, 9, 9) → 1
g0(10, 9, 10) → 1
g0(10, 9, 11) → 1
g0(11, 9, 10) → 1
g0(11, 9, 11) → 1
g0(10, 10, 9) → 1
g0(10, 11, 9) → 1
g0(11, 10, 9) → 1
g0(11, 11, 9) → 1
g0(10, 10, 10) → 1
g0(10, 10, 11) → 1
g0(10, 11, 10) → 1
g0(10, 11, 11) → 1
g0(11, 10, 10) → 1
g0(11, 10, 11) → 1
g0(11, 11, 10) → 1
g0(11, 11, 11) → 1
s0(8) → 2
s0(9) → 2
s0(10) → 2
s0(11) → 2
h0(8, 0) → 3
h0(0, 8) → 3
h0(9, 0) → 3
h0(0, 9) → 3
h0(10, 0) → 3
h0(0, 10) → 3
h0(11, 0) → 3
h0(0, 11) → 3
h0(8, 8) → 3
h0(8, 9) → 3
h0(8, 10) → 3
h0(8, 11) → 3
h0(9, 8) → 3
h0(10, 8) → 3
h0(11, 8) → 3
h0(9, 9) → 3
h0(9, 10) → 3
h0(9, 11) → 3
h0(10, 9) → 3
h0(11, 9) → 3
h0(10, 10) → 3
h0(10, 11) → 3
h0(11, 10) → 3
h0(11, 11) → 3
f0(8, 0) → 4
f0(0, 8) → 4
f0(9, 0) → 4
f0(0, 9) → 4
f0(10, 0) → 4
f0(0, 10) → 4
f0(11, 0) → 4
f0(0, 11) → 4
f0(8, 8) → 4
f0(8, 9) → 4
f0(8, 10) → 4
f0(8, 11) → 4
f0(9, 8) → 4
f0(10, 8) → 4
f0(11, 8) → 4
f0(9, 9) → 4
f0(9, 10) → 4
f0(9, 11) → 4
f0(10, 9) → 4
f0(11, 9) → 4
f0(10, 10) → 4
f0(10, 11) → 4
f0(11, 10) → 4
f0(11, 11) → 4
g1(8, 6, 7) → 1
g1(5, 9, 7) → 1
g1(5, 6, 10) → 1
g1(8, 9, 7) → 1
g1(8, 6, 10) → 1
g1(5, 9, 10) → 1
g1(8, 9, 10) → 1

(26) BOUNDS(O(1), O(n^1))